\subsection{The Brouwer--Heyting--Kolmogorov interpretation}
We will construct a system of logic in which every proof contains evidence of its truth.
Our system will have the following properties, known as the Brouwer--Heyting--Kolmogorov interpretation.
\begin{enumerate}
    \item \( \bot \) has no proof.
    \item To prove \( \varphi \wedge \psi \), one must provide a proof of \( \varphi \) together with a proof of \( \psi \).
    \item To prove \( \varphi \to \psi \), one must provide a mechanism for translating a proof of \( \varphi \) into a proof of \( \psi \).
    In particular, to prove \( \neg\varphi \), we must provide a way to turn a proof of \( \varphi \) into a contradiction.
    \item To prove \( \varphi \vee \psi \), we must specify either \( \varphi \) or \( \psi \), and then provide a proof for it.
    Note that in a classical setting, a proof of \( \varphi \vee \psi \) need not specify which of the two disjuncts is true.
    \item The law of the excluded middle \( \mathsf{LEM} \), which states \( \varphi \vee \neg \varphi \), is not valid.
    If this held for some proposition, we could decide whether the proposition was true or its negation is true, because any proof of \( \varphi \vee \neg \varphi \) contains this information.
    \item To prove \( \exists x.\, \varphi(x) \), one must provide a term \( t \) together with a proof of \( \varphi(t) \).
    \item To prove \( \forall x.\, \varphi(x) \), one must provide a mechanism that converts any term \( t \) into a proof of \( \varphi(t) \).
\end{enumerate}
This will be called \emph{intuitionistic (propositional) logic} \( \mathsf{IPC} \).
\begin{theorem}[Diaconescu]
    In intuitionistic \( \mathsf{ZF} \) set theory, the law of the excluded middle \( \mathsf{LEM} \) can be deduced from the axiom of choice \( \mathsf{AC} \).
\end{theorem}
\begin{proof}
    Let \( \varphi \) be a proposition; we want a proof of \( \varphi \vee \neg \varphi \).
    Using the axiom of separation, we have proofs that the following sets exist.
    \[ A = \qty{x \in \qty{0, 1} \mid \varphi \vee (x = 0)};\quad B = \qty{x \in \qty{0, 1} \mid \varphi \vee (x = 1)} \]
    These sets are \emph{inhabited}: there exists an element in each of them; in particular, \( 0 \in A \) and \( 1 \in A \) are intuitionistically valid.
    Note that being inhabited is strictly stronger than being nonempty in intuitionistic logic.
    This is because any proof that a set is inhabited contains information about an element in the set.
    The set \( \qty{A, B} \) is a family of inhabited sets, so by the axiom of choice, we have a choice function \( f : \qty{A, B} \to A \cup B \), and we have a proof that \( f(A) \in A \) and \( f(B) \in B \).
    Thus, we have a proof of
    \[ (\varphi \vee (f(A) = 0)) \wedge (\varphi \vee (f(B) = 1)) \]
    We also have a proof that \( f(A), f(B) \in \qty{0,1} \).
    In particular, we either have a proof that \( f(A) = 0 \) or we have a proof that \( f(A) = 1 \), and the same holds for \( B \).
    We have the following cases.
    \begin{enumerate}
        \item Suppose we have a proof that \( f(A) = 1 \).
        Then we have a proof of \( \varphi \vee (1 = 0) \), so we must have a proof of \( \varphi \).
        \item Suppose we have a proof that \( f(B) = 0 \).
        Then similarly we have a proof of \( \varphi \vee (0 = 1) \), so we must have a proof of \( \varphi \).
        \item Suppose we have proofs that \( f(A) = 0 \) and \( f(B) = 1 \).
        We will prove \( \neg \varphi \).
        Suppose that we have a proof of \( \varphi \).
        Then from a proof of \( \varphi \vee (x = 0) \) or \( \varphi \vee (x = 1) \) we can derive a proof of the other, so by the axiom of extensionality, \( A = B \).
        Then \( 0 = f(A) = f(B) = 1 \) as \( f \) is a function, giving a contradiction.
        Thus, we have constructed a proof of \( \neg\varphi \).
    \end{enumerate}
    We can always specify a proof of \( \varphi \) or a proof of \( \neg \varphi \), so we have \( \varphi \vee \neg \varphi \).
\end{proof}
\begin{remark}
    \begin{enumerate}
        \item Intuitionistic mathematics is more general than classical mathematics, because it operates on fewer assumptions.
        \item Notions that are classically conflated may be different in intuitionistic logic.
        For example, there is no classical distinction between inhabited and nonempty sets, but they are not the same in intuitionistic logic.
        Other examples include finiteness, or disequality and apartness.
        \item Intuitionistic proofs have computational content attached to them, but classical proofs may not.
        \item Intuitionistic logic is the internal logic of an arbitrary topos.
        % look at the Zariski topos
    \end{enumerate}
\end{remark}

\subsection{Natural deduction}
We will use the notation \( \Gamma \vdash \varphi \), or \( \Gamma \vdash_{\mathsf{IPC}} \varphi \), to denote that the set of \emph{open assumptions} \( \Gamma \) let us conclude \( \varphi \).
\( \Gamma \) is also called the \emph{context}.
We will inductively define this provability relation.
Some rules, called \emph{introduction rules}, let us construct proofs.
\begin{mathpar}
    \inferrule[\( \wedge \)-I]{\Gamma \vdash A \and \Gamma \vdash B}{\Gamma \vdash A \wedge B}
    \and
    \inferrule[\( \vee \)-I]{\Gamma \vdash A}{\Gamma \vdash A \vee B}
    \and
    \inferrule[\( \vee \)-I]{\Gamma \vdash B}{\Gamma \vdash A \vee B}
\end{mathpar}
Dually, some rules, called \emph{elimination rules}, let us extract information from proofs.
\begin{mathpar}
    \inferrule[\( \wedge \)-E]{\Gamma \vdash A \wedge B}{\Gamma \vdash A}
    \and
    \inferrule[\( \wedge \)-E]{\Gamma \vdash A \wedge B}{\Gamma \vdash B}
    \and
    \inferrule[\( \vee \)-E]{\Gamma, A \vdash C \and \Gamma, B \vdash C \and \Gamma \vdash A \vee B}{\Gamma \vdash C}
\end{mathpar}
We now define the principle of explosion, which is an elimination rule for \( \bot \).
We do not construct an introduction rule for \( \bot \).
\[ \inferrule[\( \bot \)-E]{\Gamma \vdash \bot}{\Gamma \vdash A} \]
We now define the introduction and elimination rules for implication.
The elimination rule is known as \emph{modus ponens}.
\begin{mathpar}
    \inferrule[\( \to \)-I]{\Gamma, A \vdash B}{\Gamma \vdash A \to B}
    \and
    \inferrule[\( \to \)-E]{\Gamma \vdash A \to B \and \Gamma \vdash A}{\Gamma \vdash B}
\end{mathpar}
We finally define a rule called the \emph{axiom schema}, that allows us to prove our assumptions.
\[ \inferrule[Ax]{\ }{\Gamma, A \vdash A} \]
If an inference rule moves an assumption out of the context, we say that the assumption is \emph{discharged} or \emph{closed}.
We are allowed to drop assumptions that we do not use; this is called the \emph{weakening} rule.
We obtain classical propositional logic \( \mathsf{CPC} \) by additionally adding one of the following two rules.
\begin{mathpar}
    \inferrule[\( \mathsf{LEM} \)]{\ }{\Gamma \vdash A \vee \neg A}
    \and
    \inferrule[\( \neg\neg \)-E]{\Gamma, \neg A \vdash \bot}{\Gamma \vdash A}
\end{mathpar}
We will additionally use the informal notation
\[ \inferrule*[right={\( (A, B) \)}]{{\begin{matrix} [A]\\\vdots\\X \end{matrix}} \and {\begin{matrix} [B]\\\vdots\\Y \end{matrix}}}{C} \]
to mean that if we can prove \( X \) assuming \( A \) and we can prove \( Y \) assuming \( B \), then we can infer \( C \) by discharging the open assumptions \( A \) and \( B \).
For example, we can write an instance of \( \to \)-I as
\[ \inferrule*[right={\( (A) \)}]{\ {\begin{matrix} \Gamma, [A]\\\vdots\\B \end{matrix}}\ }{\Gamma \vdash A \to B} \]
To extend this to intuitionistic predicate logic \( \mathsf{IQC} \), we need to add rules for quantifiers.
\begin{mathpar}
    \inferrule[\( \exists \)-I]{\Gamma \vdash \varphi[x \coloneq t]}{\Gamma \vdash \exists x.\, \varphi(x)}
    \and
    \inferrule[\( \forall \)-I]{\Gamma \vdash \varphi \and x \text{ not free in } \Gamma}{\Gamma \vdash \forall x.\, \varphi}
    \\\\
    \inferrule[\( \exists \)-E]{\Gamma \vdash \exists x.\, \varphi \and \Gamma, \varphi \vdash \psi \and x \text{ not free in } \Gamma}{\Gamma \vdash \psi}
    \and
    \inferrule[\( \forall \)-E]{\Gamma \vdash \forall x.\, \varphi}{\Gamma \vdash \varphi[x \coloneq t]}
\end{mathpar}
\begin{example}
    We will show that \( \vdash_{\mathsf{IPC}} A \wedge B \to B \wedge A \).
    \[ \inferrule*[right=\( \to \)-I]{\inferrule*[right=\( \wedge \)-I]{
        \inferrule*[right=\( \wedge \)-E]{[A \wedge B]}{B}
        \and
        \inferrule*[right=\( \wedge \)-E]{[A \wedge B]}{A}
    }{B \wedge A}}{A \wedge B \to B \wedge A} \]
\end{example}
\begin{example}
    We will show that the logical axioms
    \[ \varphi \to (\psi \to \varphi);\quad (\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi)) \]
    are intuitionistically valid.
    \[ \inferrule*[right={(\( \to \)-I, \( \varphi \))}]{
        \inferrule*[right={(\( \to \)-I, \( \psi \))}]{
            \inferrule*[right=Ax]{[\varphi]}{\varphi} \and [\psi]
        }{\psi \to \varphi}
    }{\varphi \to (\psi \to \varphi)} \]
    For the second axiom,
    \[ \inferrule*[right=\( (\varphi \to (\psi \to \chi)) \)]{
        \inferrule*[right=\( (\varphi \to \psi) \)]{
            \inferrule*[right=\( (\varphi) \)]{
                \inferrule*[right=\( \to \)-E]{
                    \inferrule*[right=\( \to \)-E]{[\varphi \to (\psi \to \chi)] \and [\varphi]}{\psi \to \chi}
                    \and
                    \inferrule*[right=\( \to \)-E]{[\varphi \to \psi] \and [\varphi]}{\psi}
                }{\chi}
            }{\varphi \to \chi}
        }{(\varphi \to \psi) \to (\varphi \to \chi)}
    }{(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))} \]
\end{example}
\begin{lemma}
    If \( \Gamma \vdash_{\mathsf{IPC}} \varphi \), then \( \Gamma, \psi \vdash_{\mathsf{IPC}} \varphi \).
    Moreover, if \( p \) is a primitive proposition and \( \psi \) is any proposition, then
    \[ \Gamma[p \coloneq \psi] \vdash_{\mathsf{IPC}} \varphi[p \coloneq \psi] \]
\end{lemma}
\begin{proof}
    This follows easily by induction over the length of the proof.
\end{proof}

\subsection{The simply typed lambda calculus}
For now, we will assume we are given a set \( \Pi \) of \emph{simple types}, generated by the grammar
\[ \Pi \Coloneq \mathcal U \mid \Pi \to \Pi \]
where \( \mathcal U \) is a countable set of \emph{primitive types} or \emph{type variables}.

Let \( V \) be an infinite set of variables.
The set \( \Lambda_\Pi \) of \emph{simply typed \( \lambda \)-terms} is defined by the grammar
\[ \Lambda_\Pi \Coloneq V \mid \underbrace{\lambda V : \Pi .\, \Lambda_\Pi}_{\text{\( \lambda \)-abstraction}} \mid \underbrace{\Lambda_\Pi \, \Lambda_\Pi}_{\text{\( \lambda \)-application}} \]

A \emph{context} \( \Gamma \) is a set of pairs \( \qty{x_1 : \tau_1, \dots, x_n : \tau_n} \), where the \( x_i \) are distinct variables, and the \( \tau_n \) are types.
We write \( \mathcal C \) for the set of all contexts.
Given a context \( \Gamma \in \mathcal C \), we also write \( \Gamma, x : \tau \) for the context \( \Gamma \cup \qty{x : \tau} \).
The \emph{domain} of \( \Gamma \) is the set \( \dom \Gamma \) of variables that appear in \( \Gamma \); similarly, the \emph{range} of \( \Gamma \) is the set \( \abs{\Gamma} \) of types that appear in \( \Gamma \).

The \emph{typability relation} \( (-) \Vdash (-) : (-) \) is a relation on \( \mathcal C \times \Lambda_\Pi \times \Pi \), defined recursively using the following rules.
\begin{enumerate}
    \item For every context \( \Gamma \), variable \( x \notin \dom \Gamma \), and type \( \tau \), we have \( \Gamma, x : \tau \Vdash x : \tau \).
    \item Let \( \Gamma \) be a context, \( x \notin \dom \Gamma \), let \( \sigma, \tau \) be types, and let \( M \) be a \( \lambda \)-term.
    If \( \Gamma, x : \sigma \Vdash M : \tau \), then \( \Gamma \Vdash (\lambda x : \sigma.\, M) : \sigma \to \tau \).
    \item Let \( \Gamma \) be a context, \( \sigma, \tau \) be types, and let \( M \) and \( N \) be \( \lambda \)-terms.
    If \( \Gamma \Vdash M : (\sigma \to \tau) \) and \( \Gamma \Vdash N : \sigma \), then \( \Gamma \Vdash (M\, N) : \tau \).
\end{enumerate}
We will refer to the \( \lambda \)-calculus of \( \Lambda_\Pi \) with this typability relation as \( \lambda(\to) \).

An occurrence of a variable \( x \) in a \( \lambda \)-abstraction is called \emph{bound}, otherwise it is called \emph{free}.
A term with no free variables is called \emph{closed}.
\( \lambda \)-terms that differ only in the names of bound variables are called \emph{\( \alpha \)-equivalent}, so for example, \( (\lambda x:\sigma.\, x) \) and \( (\lambda y:\sigma.\, y) \) are \( \alpha \)-equivalent.
Whenever it is convenient, we will replace terms with \( \alpha \)-equivalent terms to avoid reusing variable names.

If \( M \) and \( N \) are \( \lambda \)-terms and \( x \) is a variable, we can define the \emph{substitution} of \( N \) for \( x \) in \( M \) recursively:
\begin{enumerate}
    \item \( x[x \coloneq N] = N \);
    \item \( y[x \coloneq N] = y \) if \( x \neq y \);
    \item \( (\lambda y : \sigma.\, M)[x \coloneq N] = (\lambda y:\sigma.\, M[x \coloneq N]) \) if \( x \neq y \) (which can be done without loss of generality by \( \alpha \)-equivalence);
    \item \( (P\, Q)[x \coloneq N] = (P[x \coloneq N])\, (Q[x \coloneq N]) \).
\end{enumerate}

We define the \emph{\( \beta \)-reduction} relation \( \to_\beta \) on \( \Lambda_\Pi \) to be the smallest relation that is closed under the following rules:
\begin{enumerate}
    \item \( (\lambda x:\sigma.\, P)\, Q \to_\beta P[x \coloneq Q] \);
    \item if \( P \to_\beta P' \), then for any \( x \in V \) and \( \sigma \in \Pi \), we have \( (\lambda x:\sigma.\, P) \to_\beta (\lambda x:\sigma.\, P') \);
    \item if \( P \to_\beta P' \) and \( Z \) is a \( \lambda \)-term, then \( P\,Z \to_\beta P'\,Z \) and \( Z\,P \to_\beta Z\,P' \).
\end{enumerate}
We define the \emph{\( \beta \)-equivalence} relation \( \equiv_\beta \) to be the smallest equivalence relation containing \( \to_\beta \).
For example, we have
\[ (\lambda x:\mathbb Z.\, (\lambda y:\tau.\, x))\, 2 \to_\beta (\lambda y:\tau.\, 2) \]

An expression \( (\lambda x:\sigma.\, P)\, Q \) to be \( \beta \)-reduced is called a \emph{\( \beta \)-redex}; the resulting term \( P[x \coloneq Q] \) is called its \emph{\( \beta \)-reduct} or \emph{\( \beta \)-contractum}.
If no \( \beta \)-reductions can be carried out on a \( \lambda \)-term, we say that the term is in \emph{\( \beta \)-normal form}.
We write \( M \twoheadrightarrow_\beta N \) if \( M \) reduces to \( N \) after potentially multiple applications of \( \beta \)-reduction.

If \( x \) is not free in \( P \), the term \( (\lambda x:\sigma.\, (P\, x)) \) is said to \emph{\( \eta \)-reduce} to \( P \), written \( (\lambda x:\sigma.\, (P\, x)) \to_\eta P \), and we say that \( (\lambda x:\sigma.\, (P\, x)) \) and \( P \) are \emph{\( \eta \)-equivalent}.

By convention, we will write
\begin{enumerate}
    \item \( KLM \) for \( (KL)M \);
    \item \( \lambda x:\sigma.\, \lambda y:\tau.\, M \) for \( \lambda x:\sigma.\, (\lambda y:\tau.\, M) \);
    \item \( \lambda x:\sigma.\, M\, N \) for \( \lambda x:\sigma.\, (M\, N) \);
    \item \( M\, \lambda x:\sigma.\, N \) for \( M\, (\lambda x:\sigma.\, N) \).
\end{enumerate}

\subsection{Basic properties}
The following technical lemmas can be proven by induction.
\begin{lemma}[free variables lemma]
    Suppose that \( \Gamma \Vdash M : \sigma \).
    Then
    \begin{enumerate}
        \item if \( \Gamma \subseteq \Delta \), then \( \Delta \Vdash M : \sigma \);
        \item the free variables of \( M \) occur in \( \Gamma \);
        \item \( \Delta \Vdash M : \sigma \) for some \( \Delta \subseteq \Gamma \) containing only the free variables of \( M \) in its domain.
    \end{enumerate}
\end{lemma}
\begin{lemma}[generation lemma]
    \begin{enumerate}
        \item For every variable \( x \), context \( \Gamma \), and type \( \sigma \), if \( \Gamma \Vdash x : \sigma \), then \( x : \sigma \in \Gamma \).
        \item If \( \Gamma \Vdash (\lambda x: \tau.\, N) : \sigma \), then there is a type \( \rho \) such that \( \Gamma, x : \tau \Vdash N : \rho \), and \( \sigma = (\tau \to \rho) \).
        \item If \( \Gamma \Vdash (M\, N) : \sigma \), then there is a type \( \tau \) such that \( \Gamma \Vdash M : \tau \to \sigma \) and \( \Gamma \Vdash N : \tau \).
    \end{enumerate}
\end{lemma}
\begin{lemma}[substitution lemma]
    The typability relation respects substitution.
\end{lemma}
\begin{lemma}[subject reduction]
    If \( \Gamma \Vdash M : \sigma \) and \( M \to_\beta N \), then \( \Gamma \Vdash N : \sigma \).
\end{lemma}
The following theorem establishes the \emph{confluence} property of \( \lambda \)-terms.
\begin{theorem}[Church--Rosser theorem for \( \lambda(\to) \)]
    Suppose that \( \Gamma \Vdash M : \sigma \).
    If \( M \twoheadrightarrow_\beta N_1 \) and \( M \twoheadrightarrow_\beta N_2 \), then there exists \( P \) such that \( N_1 \twoheadrightarrow_\beta L \) and \( N_2 \twoheadrightarrow_\beta L \), and \( \Gamma \Vdash L : \sigma \).
    % https://q.uiver.app/#q=WzAsNCxbMSwwLCJNIl0sWzAsMSwiTl8xIl0sWzEsMiwiTCJdLFsyLDEsIk5fMiJdLFswLDEsIiIsMCx7InN0eWxlIjp7ImhlYWQiOnsibmFtZSI6ImVwaSJ9fX1dLFsxLDIsIiIsMCx7InN0eWxlIjp7ImhlYWQiOnsibmFtZSI6ImVwaSJ9fX1dLFswLDMsIiIsMix7InN0eWxlIjp7ImhlYWQiOnsibmFtZSI6ImVwaSJ9fX1dLFszLDIsIiIsMix7InN0eWxlIjp7ImhlYWQiOnsibmFtZSI6ImVwaSJ9fX1dXQ==
\[\begin{tikzcd}
	& M \\
	{N_1} && {N_2} \\
	& L
	\arrow[two heads, from=1-2, to=2-1]
	\arrow[two heads, from=2-1, to=3-2]
	\arrow[two heads, from=1-2, to=2-3]
	\arrow[two heads, from=2-3, to=3-2]
\end{tikzcd}\]
\end{theorem}
% TODO: Fill in from guided ES4 question
\begin{corollary}
    If a simply typed \( \lambda \)-term admits a \( \beta \)-normal form, then this \( \beta \)-normal form is unique.
\end{corollary}
\begin{proposition}[uniqueness of types]
    \begin{enumerate}
        \item Suppose \( \Gamma \Vdash M : \sigma \) and \( \Gamma \Vdash M : \tau \).
        Then \( \sigma = \tau \).
        \item Suppose \( \Gamma \Vdash M : \sigma \) and \( \Gamma \Vdash N : \tau \), and that \( M \equiv_\beta N \).
        Then \( \sigma = \tau \).
    \end{enumerate}
\end{proposition}
\begin{proof}
    The first part is by induction on \( M \).
    For the second part, by the Church--Rosser theorem there is a term \( L \) to which \( M \) and \( N \) both eventually reduce, so the result holds by subject reduction.
\end{proof}
\begin{example}
    There is no way to assign a type to the expression \( \lambda x.\, x\, x \).
    Indeed, if \( x \) has type \( \tau \), then it must also have type \( \tau \to \sigma \) for some \( \sigma \), but this contradicts uniqueness of types.
\end{example}

\subsection{\texorpdfstring{\( \beta \)}{β}-normal form}
We will measure the complexity of a type by looking at it as a binary tree.
For example, for
\[ \rho = \mu \to [((\varphi \to \psi) \to \chi) \to ((\varphi \to \chi) \to (\varphi \to \psi))] \]
the corresponding binary tree is
% https://q.uiver.app/#q=WzAsMTUsWzIsNCwiXFxidWxsZXQiXSxbMSwzLCJcXG11Il0sWzMsMywiXFxidWxsZXQiXSxbMiwyLCJcXGJ1bGxldCJdLFsxLDEsIlxcYnVsbGV0Il0sWzMsMSwiXFxjaGkiXSxbMCwwLCJcXHZhcnBoaSJdLFsyLDAsIlxccHNpIl0sWzUsMiwiXFxidWxsZXQiXSxbNCwxLCJcXGJ1bGxldCJdLFszLDAsIlxcdmFycGhpIl0sWzUsMCwiXFxjaGkiXSxbNywxLCJcXGJ1bGxldCJdLFs2LDAsIlxcdmFycGhpIl0sWzgsMCwiXFxwc2kiXSxbMCwxXSxbMCwyXSxbMiwzXSxbMyw0XSxbMyw1XSxbNCw2XSxbNCw3XSxbMiw4XSxbOCw5XSxbOSwxMF0sWzksMTFdLFs4LDEyXSxbMTIsMTNdLFsxMiwxNF1d
\[\begin{tikzcd}
	\varphi && \psi & \varphi && \chi & \varphi && \psi \\
	& \bullet && \chi & \bullet &&& \bullet \\
	&& \bullet &&& \bullet \\
	& \mu && \bullet \\
	&& \bullet
	\arrow[from=5-3, to=4-2]
	\arrow[from=5-3, to=4-4]
	\arrow[from=4-4, to=3-3]
	\arrow[from=3-3, to=2-2]
	\arrow[from=3-3, to=2-4]
	\arrow[from=2-2, to=1-1]
	\arrow[from=2-2, to=1-3]
	\arrow[from=4-4, to=3-6]
	\arrow[from=3-6, to=2-5]
	\arrow[from=2-5, to=1-4]
	\arrow[from=2-5, to=1-6]
	\arrow[from=3-6, to=2-8]
	\arrow[from=2-8, to=1-7]
	\arrow[from=2-8, to=1-9]
\end{tikzcd}\]
The height of this tree is the complexity of the type, which in this case is 4.
For convenience, we will annotate types of terms with superscripts.
\begin{definition}
    The \emph{height} function is the map \( h : \Pi \to \mathbb N \) that maps a type variable to 0, and maps a function type \( \sigma \to \tau \) to \( 1 + \max(h(\sigma), h(\tau)) \).
    We extend the height function to \( \beta \)-redexes: if \( (\lambda x:\sigma.\, P^\tau)^{\sigma \to \tau} R^\sigma \) is a redex, its height is \( h(\sigma \to \tau) \).
\end{definition}
\begin{theorem}[weak normalisation theorem]
    Suppose \( \Gamma \Vdash M : \sigma \).
    Then there is a finite reduction path
    \[ M = M_0 \to_\beta M_1 \to_\beta \dots \to_\beta M_n \]
    where \( M_n \) is in \( \beta \)-normal form.
\end{theorem}
\begin{proof}[Proof (taming the hydra)]
    First, we define the function \( m : \Lambda_\Pi \to \mathbb N \times \mathbb N \) by \( m(M) = (0, 0) \) if \( M \) is in \( \beta \)-normal form, and otherwise, \( m(M) \) is the pair \( (h(M), \operatorname{redex}(M)) \) where \( h(M) \) is the maximal height of redexes in \( M \) and \( \operatorname{redex}(M) \) is the number of redexes in \( M \).
    We will use induction on the well-founded relation given by the lexicographic order on \( \mathbb N \times \mathbb N \) to show that if \( M \) is typeable, it can be reduced to \( \beta \)-normal form.

    If \( \Gamma \Vdash M : \sigma \) and \( M \) is in \( \beta \)-normal form, then the claim is trivial.
    Otherwise, let \( \Delta \) be the rightmost redex of maximal height \( h = h(M) \).
    By reducing \( \Delta \), we may introduce copies of existing redexes, or create new redexes.
    Creation of new redexes can occur in one of the following ways.
    \begin{enumerate}
        \item Suppose \( \Delta \) is of the form
        \[ (\lambda x:(\rho \to \mu).\, \dots x\, P^\rho \dots)(\lambda y:\rho.\, Q^\mu)^{\rho \to \mu} \]
        Then it reduces to
        \[ \dots (\lambda y:\rho.\, Q^\mu)^{\rho \to \mu} P^\rho \dots \]
        which is a new redex of height \( h(\rho \to \mu) < h \).
        \item Suppose \( \Delta \) is of the form
        \[ (\lambda x:\tau.\, \lambda y:\rho.\, R^\mu)P^\tau \]
        occurring in the position \( \Delta^{\rho \to \tau}\, Q^\rho \).
        Suppose that \( \Delta \) reduces to \( \lambda y:\rho.\, R^\mu_1 \).
        Then we have created a new redex \( (\lambda y:\rho.\, R^\mu_1) Q^\rho \) of height \( h(\rho \to \mu) < h(\tau \to \rho \to \mu) = h \).
        \item Suppose \( \Delta \) is of the form
        \[ (\lambda x:(\rho \to \mu).\, x)(\lambda y:\rho.\, P^\mu) \]
        occurring in the position \( \Delta^{\rho \to \mu} Q^\rho \).
        Then this reduces to \( (\lambda y:\rho.\, P^\mu) Q^\rho \) of height \( h(\rho \to \mu) < h \).
    \end{enumerate}
    There is still the possibility that reduction of \( \Delta \) introduces copies of existing redexes.
    Suppose \( \Delta \) is of the form
    \[ (\lambda x: \rho.\, P^\rho) Q^\tau \]
    and \( P \) has more than one free occurrence of \( x \).
    Then the reduction of \( \Delta \) will copy all redexes in \( Q \).
    But as \( \Delta \) was chosen to be rightmost with maximal height, the height of all redexes in \( Q \) have height less than \( h \).

    So if \( M \to_\beta M' \) by reducing \( \Delta \), it is always the case that \( m(M') < m(M) \) in the lexicographic order.
    By the inductive hypothesis, \( M' \) can be reduced to \( \beta \)-normal form, so the result also holds for \( M \).
\end{proof}
\begin{theorem}[strong normalisation theorem]
    Let \( \Gamma \Vdash M : \sigma \).
    Then there is no infinite sequence
    \[ M \to_\beta M_1 \to_\beta M_2 \to_\beta \cdots \]
\end{theorem}
The proof is omitted.

\subsection{Propositions as types}
We will work with the fragment of \( \mathsf{IPC} \), denoted \( \mathsf{IPC}(\to) \), where the only connective is \( \to \), and the deduction rules are \( \to \)-I, \( \to \)-E, \textsc{Ax}.

If \( \mathcal L \) is a propositional language for \( \mathsf{IPC}(\to) \) and \( P \) is its set of primitive propositions, we can generate a simply typed \( \lambda \)-calculus \( \lambda(\to) \) by taking the set of primitive types \( \mathcal U \) to be \( P \).
Then the types \( \Pi \) and the propositions \( \mathcal L \) are generated by the same grammar
\[ \mathcal U \mid \Pi \to \Pi \]
A proposition is thus the type of its proofs, and a context is a set of hypotheses.
\begin{proposition}[Curry--Howard correspondence for \( \mathsf{IPC}(\to) \)]
    Let \( \Gamma \) be a context for \( \lambda(\to) \), and let \( \varphi \) be a proposition.
    Then
    \begin{enumerate}
        \item If \( \Gamma \Vdash M : \varphi \), then
        \[ \abs{\Gamma} = \qty{\tau \in \Pi \mid \exists x.\, (x : \tau) \in \Gamma} \vdash_{\mathsf{IPC}(\to)} \varphi \]
        \item If \( \Gamma \vdash_{\mathsf{IPC}(\to)} \varphi \), then there is a simply typed \( \lambda \)-term \( M \) such that
        \[ \qty{(x_\tau : \tau) \mid \tau \in \Gamma} \Vdash M : \varphi \]
    \end{enumerate}
\end{proposition}
\begin{proof}
    \emph{Part (i).}
    We use induction over the derivation of \( \Gamma \Vdash M : \varphi \).
    If \( x \) is a variable not occurring in \( \Gamma' \), and the derivation is of the form \( \Gamma', x : \varphi \Vdash x : \varphi \), then we must prove that \( \abs{\Gamma', x : \varphi} \vdash \varphi \), and this holds as \( \varphi \vdash \varphi \).

    If the derivation has \( M \) of the form \( \lambda x:\sigma.\, N \) and \( \varphi = \sigma \to \tau \), then we must have that \( \Gamma, x: \sigma \Vdash N : \tau \).
    By the inductive hypothesis, we have \( \abs{\Gamma, x : \sigma} \vdash \tau \), so \( \abs{\Gamma}, \sigma \vdash \tau \).
    Thus we obtain a proof of \( \sigma \to \tau \) from \( \abs{\Gamma} \) by \( \to \)-I.

    If the derivation is of the form \( \Gamma \Vdash (P\, Q) : \varphi \), then we must have \( \Gamma \Vdash P : \sigma \to \varphi \) and \( \Gamma \Vdash Q : \sigma \) for some \( \sigma \).
    By the inductive hypothesis, \( \abs{\Gamma} \vdash \sigma \to \varphi \) and \( \abs{\Gamma} \vdash \sigma \).
    Then the result holds by \( \to \)-E.

    \emph{Part (ii).}
    We use induction over the proof tree of \( \Gamma \vdash_{\mathsf{IPC}(\to)} \varphi \).
    We write
    \[ \Delta = \qty{(x_\tau : \tau) \mid \tau \in \Gamma} \]
    Suppose that we are at a stage of the proof that uses \textsc{Ax}, so \( \Gamma, \varphi \vdash \varphi \).
    If \( \varphi \in \Gamma \), then clearly \( \Delta \Vdash x_\varphi : \varphi \).
    Otherwise, \( \Delta, x_\varphi : \varphi \Vdash x_\varphi : \varphi \) as required.

    Suppose that we are at a stage of the proof that uses \( \to \)-E, so
    \[ \inferrule{\Gamma \vdash \varphi \to \psi \and \Gamma \vdash \varphi}{\Gamma \vdash \psi} \]
    By the inductive hypothesis, there are \( \lambda \)-terms \( M, N \) such that \( \Delta \Vdash M : \varphi \to \psi \) and \( \Delta \Vdash N : \varphi \).
    Then \( \Delta \Vdash (M\, N) : \psi \) as required.

    Finally, suppose we are at a stage of the proof that uses \( \to \)-I, so
    \[ \inferrule{\Gamma, \varphi \vdash \psi}{\Gamma \vdash \varphi \to \psi} \]
    If \( \varphi \in \Gamma \), then by the inductive hypothesis, there is a \( \lambda \)-term \( M \) such that \( \Delta \Vdash M : \psi \).
    By the weakening rule, \( \Delta, x : \varphi \Vdash M : \psi \) where \( x \) is a variable that does not occur in \( \Delta \).
    Then \( \Delta \Vdash (\lambda x:\varphi.\, M) : \varphi \to \psi \) as required.
    Now suppose \( \varphi \notin \Gamma \).
    By the inductive hypothesis we obtain a \( \lambda \)-term \( M \) such that \( \Delta, x_\varphi : \varphi \Vdash M : \psi \).
    Then similarly \( \Delta \Vdash (\lambda x_\varphi:\varphi.\, M) : \varphi \to \psi \).
\end{proof}
This justifies the Brouwer--Heyting--Kolmogorov interpretation of intuitionistic logic.
\begin{example}
    Let \( \varphi, \psi \) be primitive propositions, and consider the \( \lambda \)-term
    \[ \lambda f:(\varphi \to \psi) \to \varphi.\,\lambda g: \varphi \to \psi.\, g(fg) \]
    This term has type
    \[ ((\varphi \to \psi) \to \varphi) \to ((\varphi \to \psi) \to \psi) \]
    The term encodes a proof of this proposition in \( \vdash_{\mathsf{IPC}(\to)} \).
    The corresponding proof tree is
    \[ \inferrule*[right=\( \to \)-I]
        {\inferrule*[right=\( \to \)-I]{\inferrule*[right=\( \to \)-E]{
            \inferrule*[right=\( \to \)-E]{g : [\varphi \to \psi] \and f : [(\varphi \to \psi) \to \varphi]}{fg : \varphi}
        \and g : [\varphi \to \psi]}{g(fg) : \psi}}
        {\lambda g: \varphi \to \psi.\, g(fg) : (\varphi \to \psi) \to \psi}}
        {\lambda f:(\varphi \to \psi) \to \varphi.\,\lambda g: \varphi \to \psi.\, g(fg) : ((\varphi \to \psi) \to \varphi) \to ((\varphi \to \psi) \to \psi)} \]
\end{example}

\subsection{Full simply typed lambda calculus}
The types of the full simply typed \( \lambda \)-calculus \( \mathsf{ST}\lambda\mathsf{C} \) are generated by the following grammar.
\[ \Pi \Coloneq \mathcal U \mid \Pi \to \Pi \mid \Pi \times \Pi \mid \Pi + \Pi \mid 1 \mid 0 \]
where \( \mathcal U \) is a set of primitive types or type variables.
The terms are of the form
\begin{align*}
    \Lambda_\Pi \Coloneq\, & V \mid (\lambda x : \Pi.\, \Lambda_\Pi) \mid \Lambda_\Pi \, \Lambda_\Pi \mid \\
    &\langle \Lambda_\Pi, \Lambda_\Pi \rangle \mid \pi_1(\Lambda_\Pi) \mid \pi_2(\Lambda_\Pi) \mid \\
    &\iota_1(\Lambda_\Pi) \mid \iota_2(\Lambda_\Pi) \mid \mathsf{case}(\Lambda_\Pi;V.\Lambda_\Pi;V.\Lambda_\Pi) \mid \\
    &\star \mid {!_\Pi\, \Lambda_\Pi}
\end{align*}
where \( V \) is an infinite set of variables, and \( \star \) is a constant.
This expanded syntax comes with new typing rules.
\begin{mathpar}
    \inferrule{\Gamma \Vdash M : \psi \times \varphi}{\Gamma \Vdash \pi_1(M) : \psi}
    \and
    \inferrule{\Gamma \Vdash M : \psi \times \varphi}{\Gamma \Vdash \pi_2(M) : \varphi}
    \and
    \inferrule{\Gamma \Vdash M : \psi \and \Gamma \Vdash N : \varphi}{\Gamma \Vdash \langle M, N \rangle : \psi \times \varphi}
    \and
    \inferrule{\Gamma \Vdash M : \psi}{\Gamma \Vdash \iota_1(M) : \psi + \varphi}
    \and
    \inferrule{\Gamma \Vdash M : \varphi}{\Gamma \Vdash \iota_2(M) : \psi + \varphi}
    \and
    \inferrule{\Gamma \Vdash L : \psi + \varphi \and \Gamma, x : \psi \Vdash M : \rho \and \Gamma, y : \varphi \Vdash N : \rho}{\Gamma \Vdash \mathsf{case}(L;x^\psi.M;y^\varphi.N) : \rho}
    \and
    \inferrule{\ }{\Gamma \Vdash \star : 1}
    \and
    \inferrule{\Gamma \Vdash M : 0}{\Gamma \Vdash !_\varphi\, M : \varphi}
\end{mathpar}
This typing relation captures the Brouwer--Heyting--Kolmogorov interpretation when paired with new reduction rules.
\begin{mathpar}
    \pi_1(\langle M, N \rangle) \to_\beta M
    \and
    \pi_2(\langle M, N \rangle) \to_\beta N
    \and
    \langle \pi_1(M), \pi_2(M) \rangle \to_\eta M
    \and
    \mathsf{case}(\iota_1(M);x^\psi.K;y^\varphi.L) \to_\beta K[x \coloneq M]
    \and
    \mathsf{case}(\iota_2(M);x^\psi.K;y^\varphi.L) \to_\beta L[y \coloneq M]
    \and
    \text{if } \Gamma \Vdash M : 1 \text{ then } M \to_\eta \star
\end{mathpar}
We can expand propositions-as-types to our new types:
\begin{enumerate}
    \item \( 0 \) corresponds to \( \bot \);
    \item \( 1 \) corresponds to \( \top \);
    \item product types correspond to conjunctions;
    \item coproduct types correspond to disjunctions.
\end{enumerate}
In this way, propositions correspond to types.
Redexes are now those expressions consisting of a constructor (pair formation, \( \lambda \)-abstraction, and injections) followed by the corresponding destructor (projections, applications, and case expressions).
\begin{example}
    Consider the following proof of \( (\varphi \wedge \chi) \to (\psi \to \varphi) \).
    \[ \inferrule{
        \inferrule{
            \inferrule{[\varphi \wedge \chi]}{\varphi} \and [\psi]
        }{\psi \to \varphi}
    }{(\varphi \wedge \chi) \to (\psi \to \varphi)} \]
    Annotating the corresponding \( \lambda \)-terms, we obtain
    \[ \inferrule{
        \inferrule{
            \inferrule{p : [\varphi \wedge \chi]}{\pi_1(p) : \varphi} \and b : [\psi]
        }{\lambda b^\psi.\, \pi_1(p) : \psi \to \varphi}
    }{\lambda p^{\varphi \times \chi}.\, \lambda b^\psi.\, \pi_1(p) : (\varphi \wedge \chi) \to (\psi \to \varphi)} \]
    Hence this proof tree corresponds to the \( \lambda \)-term
    \[ \lambda p^{\varphi \times \chi}.\, \lambda b^\psi.\, \pi_1(p) : (\varphi \times \chi) \to (\psi \to \varphi) \]
\end{example}
In summary, the Curry--Howard correspondence for the whole of \( \mathsf{IPC} \) and \( \mathsf{ST}\lambda\mathsf{C} \) states that
\begin{enumerate}
    \item (primitive) types correspond to (primitive) propositions;
    \item variables correspond to hypotheses;
    \item \( \lambda \)-terms correspond to proofs;
    \item inhabitation of a type corresponds to provability of a proposition;
    \item term reduction corresponds to proof normalisation.
\end{enumerate}

\subsection{Heyting semantics}
Boolean algebras represent truth-values of classical propositions.
We can generalise this notion to intuitionistic logic.
\begin{definition}
    A \emph{Heyting algebra} \( H \) is a bounded lattice equipped with a binary operation \( \Rightarrow : H \times H \to H \) such that
    \[ a \wedge b \leq c \iff a \leq b \Rightarrow c \]
    A \emph{morphism} of Heyting algebras is a function that preserves all finite meets and joins (including true and false) and \( \Rightarrow \).
\end{definition}
In particular, if \( f \) is a morphism of Heyting algebras and \( a \leq b \), then \( f(a) \leq f(b) \).
\begin{example}
    \begin{enumerate}
        \item Every Boolean algebra is a Heyting algebra by defining \( a \Rightarrow b \) to be \( \neg a \vee b \).
        Note that \( \neg a = a \Rightarrow \bot \).
        \item Every topology is a Heyting algebra, where \( U \Rightarrow V = ((X \setminus U) \cup V)^\circ \).
        \item Every finite distributive lattice is a Heyting algebra.
        \item The Lindenbaum--Tarski algebra of a propositional theory \( \mathcal T \) with respect to \( \mathsf{IPC} \) is a Heyting algebra.
        % important exercise
    \end{enumerate}
\end{example}
\begin{definition}
    Let \( H \) be a Heyting algebra and let \( \mathcal L \) be a propositional language with a set \( P \) of primitive propositions.
    An \emph{\( H \)-valuation} is a function \( v : P \to H \), recursively expanded to \( \mathcal L \) by the rules
    \begin{enumerate}
        \item \( v(\bot) = \bot \);
        \item \( v(A \wedge B) = v(A) \wedge v(B) \);
        \item \( v(A \vee B) = v(A) \vee v(B) \);
        \item \( v(A \to B) = v(A) \Rightarrow v(B) \).
    \end{enumerate}
    We say that a proposition \( A \) is \emph{\( H \)-valid} if \( v(A) = \top \) for all valuations \( v \).
    \( A \) is an \emph{\( H \)-consequence} of a finite set of propositions \( \Gamma \) if \( v\qty(\bigwedge \Gamma) \leq v(A) \), and write \( \Gamma \vDash_H A \).
\end{definition}
\begin{lemma}[soundness]
    Let \( H \) be a Heyting algebra and let \( v : \mathcal L \to H \) be an \( H \)-valuation.
    If \( \Gamma \vdash_{\mathsf{IPC}} A \), then \( \Gamma \vDash_H A \).
\end{lemma}
\begin{proof}
    We proceed by induction over the derivation of \( \Gamma \vdash_{\mathsf{IPC}} A \).
    \begin{enumerate}
        \item (\textsc{Ax}) \( v\qty((\bigwedge \Gamma) \wedge A) = v\qty(\bigwedge \Gamma) \wedge v(A) \leq v(A) \).
        \item (\( \wedge \)-I) In this case, \( A = B \wedge C \) and we have derivations \( \Gamma_1 \vdash B, \Gamma_2 \vdash C \) with \( \Gamma_1, \Gamma_2 \subseteq \Gamma \).
        By the inductive hypothesis, \( v(\Gamma_1) \leq v(B) \) and \( v(\Gamma_2) \leq v(C) \), hence
        \[ v\qty(\bigwedge \Gamma) \leq v(\Gamma_1) \wedge v(\Gamma_2) \leq v(B) \wedge v(C) = v(B \wedge C) = v(A) \]
        \item (\( \to \)-I) In this case, \( A = B \to C \) and we have \( \Gamma \cup \qty{B} \vdash C \).
        By the inductive hypothesis, \( v\qty(\bigwedge\Gamma) \wedge v(B) \leq v(C) \).
        But then \( v\qty(\bigwedge\Gamma) \leq v(B) \Rightarrow v(C) \) by definition, so \( v\qty(\bigwedge\Gamma) \leq v(B \to C) \) as required.
        \item (\( \vee \)-I) In this case, \( A = B \vee C \), and without loss of generality, we have \( \Gamma \vdash B \).
        By the inductive hypothesis, \( v\qty(\bigwedge \Gamma) \leq v(B) \), but \( v(B) \leq v(B) \vee v(C) = v(B \vee C) \) as required.
        \item (\( \wedge \)-E) By the inductive hypothesis, we have \( v\qty(\bigwedge \Gamma) \leq v(A \wedge B) = v(A) \wedge v(B) \leq v(A), v(B) \) as required.
        \item (\( \to \)-E) We know that \( v(A \to B) = (v(A) \Rightarrow v(B)) \).
        From the inequality \( v(A \to B) \leq (v(A) \Rightarrow v(B)) \), we deduce \( v(A \to B) \wedge v(A) \leq v(B) \).
        Thus, if \( v\qty(\bigwedge \Gamma) \leq v(A \to B) \) and \( v\qty(\bigwedge \Gamma) \leq v(A) \), we have \( v\qty(\bigwedge \Gamma) \leq v(B) \) as required.
        \item (\( \vee \)-E) By the inductive hypothesis,
        \[ v\qty(A \wedge \bigwedge \Gamma) \leq v(C);\quad v\qty(B \wedge \bigwedge \Gamma) \leq v(C);\quad v\qty(\bigwedge \Gamma) \leq v(A \vee B) = v(A) \vee v(B) \]
        Hence,
        \[ v\qty(\bigwedge \Gamma) = v\qty(\bigwedge \Gamma) \wedge (v(A) \vee v(B)) = \qty(v\qty(\bigwedge \Gamma) \wedge v(A)) \vee \qty(v\qty(\bigwedge \Gamma) \wedge v(B)) \leq v(C) \vee v(C) = v(C) \]
        as every Heyting algebra is a distributive lattice.
        \item (\( \bot \)-E) If \( v\qty(\bigwedge\Gamma) \leq v(\bot) = \bot \), then \( v\qty(\bigwedge \Gamma) = \bot \).
        Hence, \( v\qty(\bigwedge \Gamma) \leq v(A) \) for any \( A \).
    \end{enumerate}
\end{proof}
\begin{example}
    The law of the excluded middle \( \mathsf{LEM} \) is not provable in \( \mathsf{IPC} \).
    Let \( p \) be a primitive proposition, and consider the Heyting algebra given by the Sierpi\'nski topology \( \qty{\varnothing, \qty{1}, \qty{1, 2}} \) on \( X = \qty{1,2} \).
    We define the valuation given by \( v(p) = \qty{1} \).
    Then
    \[ v(\neg p) = \qty{1} \Rightarrow \varnothing = (\qty{1, 2} \setminus \qty{1})^\circ = \qty{2}^\circ = \varnothing \]
    Hence,
    \[ v(p \vee \neg p) = \qty{1} \cup \varnothing = \qty{1} \neq \qty{1, 2} = \top \]
    Thus, by soundness, \( p \vee \neg p \) is not provable (from the empty context, which has valuation \( \top = \qty{1, 2} \)) in \( \mathsf{IPC} \).
\end{example}
\begin{example}
    Peirce's law \( ((p \to q) \to p) \to p \) is not intuitionistically valid.
    Let \( H \) be the Heyting algebra given by the usual topology on the plane \( \mathbb R^2 \), and let
    \[ v(p) = \mathbb R^2 \setminus \qty{(0, 0)};\quad v(q) = \varnothing \]
    % TODO: complete
\end{example}
Classical completeness can be phrased as
\[ \Gamma \vdash_{\mathsf{CPC}} A \iff \Gamma \vDash_2 A \]
where \( 2 \) is the Boolean algebra \( \qty{0, 1} \).
For intuitionistic logic, we cannot replace \( 2 \) with a single finite Heyting algebra, so we will instead quantify over all Heyting algebras.
\begin{theorem}[completeness]
    A proposition is provable in \( \mathsf{IPC} \) if and only if it is \( H \)-valid for every Heyting algebra \( H \).
\end{theorem}
\begin{proof}
    For the forward direction, if \( \vdash_{\mathsf{IPC}} A \), then \( \top \leq v(A) \) for every Heyting algebra \( H \) and valuation \( v \), by soundness.
    Then \( \top = v(A) \), so \( A \) is \( H \)-valid.

    For the backward direction, suppose \( A \) is \( H \)-valid for every Heyting algebra \( H \).
    Note that the Lindenbaum--Tarski algebra \( \faktor{\mathcal L}{\sim} \) for the empty theory, with respect to \( \mathsf{IPC} \), is a Heyting algebra.
    Consider the valuation given by mapping each primitive proposition to its equivalence class in \( \faktor{\mathcal L}{\sim} \).
    Then, one can easily show by induction that \( v : \mathcal L \to \faktor{\mathcal L}{\sim} \) is the quotient map by considering the construction of the Lindenbaum--Tarski algebra.
    Now, \( A \) is valid in every Heyting algebra and with respect to every valuation, so in particular, \( v(A) = \top \) in \( \faktor{\mathcal L}{\sim} \).
    But then \( v(A) \in [\top] \), so \( \vdash_{\mathsf{IPC}} A \leftrightarrow \top \), so \( \vdash_{\mathsf{IPC}} A \) as required.
\end{proof}

\subsection{Kripke semantics}
\begin{definition}
    Let \( S \) be a poset.
    For each \( a \in S \), we define its \emph{principal up-set} to be
    \[ {a\!\uparrow} = \qty{s \in S \mid a \leq s} \]
\end{definition}
Note that \( U \subseteq S \) is a terminal segment if and only if it contains \( a\!\uparrow \) for each \( a \in U \).
\begin{proposition}
    Let \( S \) be a poset.
    Then the set \( T(S) \) of terminal segments of \( S \) has the structure of a Heyting algebra.
\end{proposition}
\begin{proof}
    The order is given by inclusion: \( U \leq V \) if and only if \( U \subseteq V \).
    We define
    \begin{align*}
        U \wedge V &= U \cap V \\
        U \vee V &= U \cup V \\
        U \Rightarrow V &= \qty{s \mid {s\!\uparrow} \cap U \subseteq V}
    \end{align*}
    One can check that this forms a Heyting algebra as required.
\end{proof}
\begin{definition}
    Let \( P \) be a set of primitive propositions.
    A \emph{Kripke model} is a triple \( (S, \leq, \Vdash) \) where \( S \) is a poset and \( (\Vdash) \subseteq S \times P \) is a relation satisfying the \emph{persistence property}: if \( p \in P \) is such that \( s \Vdash p \) and \( s \leq s' \), then \( s' \Vdash p \).
\end{definition}
\( S \) is a set of possible \emph{worlds}, or states of knowledge, ordered by how knowledgeable they are.
The relation \( \Vdash \) is called the \emph{forcing} relation; we say that a world \emph{forces} a proposition to be true.

Every valuation \( v \) on \( T(S) \) induces a Kripke model by setting \( s \Vdash p \iff s \in v(p) \).
The persistence property corresponds to the fact that \( T(S) \) contains only terminal segments.
\begin{definition}
    Let \( (S, \leq, \Vdash) \) be a Kripke model.
    We can extend the forcing relation to a relation \( (\Vdash) \subseteq S \times \mathcal L \) recursively as follows.
    \begin{enumerate}
        \item \( s \nVdash \bot \);
        \item \( s \Vdash \varphi \wedge \psi \) if and only if \( s \Vdash \varphi \) and \( s \Vdash \psi \);
        \item \( s \Vdash \varphi \vee \psi \) if and only if \( s \Vdash \varphi \) or \( s \Vdash \psi \);
        \item \( s \Vdash \varphi \to \psi \) if and only if for all \( s' \geq s \), \( s' \Vdash \varphi \) implies \( s' \Vdash \psi \).
    \end{enumerate}
\end{definition}
One can check by induction that persistence holds for arbitrary propositions.
\begin{remark}
    \( s \Vdash \neg\varphi \) if and only if no more knowledgeable world than \( s \) forces \( \varphi \).
    \( s \Vdash \neg\neg\varphi \) is the statement that \( \varphi \) is consistent with every extension of \( s \) but need not hold in \( s \) itself; that is, for each \( s' \geq s \), there exists \( s'' \geq s' \) with \( s \Vdash \varphi \).
\end{remark}
We say that \( S \Vdash \varphi \) if every world \( s \) forces \( \varphi \).
If \( S \) has a bottom element \( s \), then \( S \Vdash \varphi \) if and only if \( s \Vdash \varphi \) by persistence.
\begin{example}
    Consider the Kripke models
    \begin{enumerate}
        \item % https://q.uiver.app/#q=WzAsMixbMCwxLCJzIl0sWzAsMCwicyciXSxbMCwxLCIiLDAseyJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV1d
        \[\begin{tikzcd}
            {s'} \\
            s
            \arrow[no head, from=2-1, to=1-1]
        \end{tikzcd}\]
            where \( s' \Vdash p \);
        \item % https://q.uiver.app/#q=WzAsMyxbMSwxLCJzIl0sWzAsMCwicyciXSxbMiwwLCJzJyciXSxbMCwxLCIiLDAseyJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzAsMiwiIiwyLHsic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dXQ==
        \[\begin{tikzcd}
            {s'} && {s''} \\
            & s
            \arrow[no head, from=2-2, to=1-1]
            \arrow[no head, from=2-2, to=1-3]
        \end{tikzcd}\]
        where \( s'' \Vdash p \);
        \item % https://q.uiver.app/#q=WzAsMixbMCwxLCJzIl0sWzAsMCwicyciXSxbMCwxLCIiLDAseyJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV1d
        \[\begin{tikzcd}
            {s'} \\
            s
            \arrow[no head, from=2-1, to=1-1]
        \end{tikzcd}\]
            where \( s' \Vdash p \) and \( s' \Vdash q \).
    \end{enumerate}
    Note that in (i), we have \( s \nVdash \neg p \), since \( s' \geq s \) and \( s' \Vdash p \).
    But also \( s \nVdash p \) by assumption, thus \( s \nVdash p \vee \neg p \).
    Note that \( s \Vdash \neg\neg p \), but \( s \nVdash p \), so we also have \( s \nVdash \neg\neg p \to p \).

    In (ii), \( s \nVdash \neg\neg p \), since \( s' \geq s \) cannot access a world that forces \( p \).
    We also have \( s \nVdash \neg p \), since \( s'' \geq s' \) and \( s'' \vDash p \).
    Thus \( s \nVdash \neg\neg p \vee \neg p \).

    In (iii), \( s \nVdash (p \to q) \to (\neg p \vee q) \).
    Indeed, all worlds force \( p \to q \), and we have \( s \nVdash q \), so it suffices to check that \( s \nVdash \neg p \), but this holds as \( s' \geq s \) and \( s' \vDash p \).
\end{example}
A filter \( \mathcal F \) is called \emph{prime} if whenever \( x \vee y \in \mathcal F \), either \( x \in \mathcal F \) or \( y \in \mathcal F \).
\begin{lemma}
    Let \( H \) be a Heyting algebra and let \( v \) be an \( H \)-valuation.
    Then there is a Kripke model \( (S, \leq, \Vdash) \) such that for each proposition \( \varphi \), we have \( v \vDash_H \varphi \) if and only if \( S \Vdash \varphi \).
\end{lemma}
Thus we can convert between Kripke models and valuations on Heyting algebras.
This will allow us to prove the completeness theorem for Kripke semantics.
\begin{proof}
    Let \( S \) be the set of prime filters on \( H \) ordered by inclusion.
    We say that \( \mathcal F \Vdash p \) if and only if \( v(p) \in \mathcal F \), and prove by induction that this extends to arbitrary propositions.
    Here, we will prove the case of implications; the other connectives are easy, and primality of the filter is required for the case of disjunction.
    Let \( \mathcal F \Vdash (\psi \to \psi') \) and suppose \( v(\psi \to \psi') = v(\psi) \Rightarrow v(\psi') \notin \mathcal F \).
    Let \( \mathcal G' \) be the smallest filter containing \( \mathcal F \) and \( v(\psi) \).
    Then
    \[ \mathcal G' = \qty{b \mid \exists f \in \mathcal F.\, f \wedge v(\psi) \leq b} \]
    Note that \( v(\psi') \notin \mathcal G' \), otherwise \( f \wedge v(\psi) \leq v(\psi') \) for some \( f \in \mathcal F \), and then \( f \leq v(\psi) \Rightarrow v(\psi') \in \mathcal F \), giving a contradiction.
    In particular, \( \mathcal G' \) is a proper filter, so by Zorn's lemma there is a prime filter \( \mathcal G \) containing \( \mathcal G' \) that does not contain \( v(\psi') \).

    By the inductive hypothesis, \( \mathcal G \Vdash \psi \), and since \( \mathcal F \Vdash (\psi \to \psi') \) and \( \mathcal G' \) contains \( \mathcal G \) which contains \( \mathcal F \), we must have \( \mathcal G \Vdash \psi' \).
    Then \( v(\psi') \in \mathcal G \), which is a contradiction.
    Thus \( \mathcal F \Vdash \psi \to \psi' \) implies that \( v(\psi \to \psi') \in \mathcal F \).

    Conversely, suppose
    \[ v(\psi \to \psi') \in \mathcal F \subseteq \mathcal G \Vdash \psi \]
    By the inductive hypothesis, \( v(\psi) \in \mathcal G \), and so \( v(\psi) \Rightarrow v(\psi') \in \mathcal G \) as \( \mathcal F \subseteq \mathcal G \).
    Then \( v(\psi') \geq v(\psi) \wedge (v(\psi) \Rightarrow v(\psi')) \in \mathcal G \), so again by the inductive hypothesis, \( G \Vdash \psi' \) as required.

    It thus suffices to show that \( v \vDash_H \varphi \) if and only if \( S \Vdash \varphi \).
    If \( v \vDash_H \varphi \), then \( v(\varphi) = \top \), so \( v(\varphi) \) is contained in every filter of \( H \).
    So \( \mathcal F \Vdash \varphi \) for every prime filter \( \mathcal F \).
    Conversely, suppose \( S \Vdash \varphi \) but \( v \nvDash_H \varphi \).
    Then since \( v(\varphi) \neq \top \), there must be a proper filter \( \mathcal F \) that does not contain \( v(\varphi) \).
    We extend this as above to a prime filter \( \mathcal G \) that does not contain \( v(\varphi) \).
    Then \( \mathcal G \nVdash \varphi \), contradicting the assumption that \( S \Vdash \varphi \).
\end{proof}
\begin{theorem}[completeness]
    For every proposition \( \varphi \), we have \( \Gamma \vdash_{\mathsf{IPC}} \varphi \) if and only if for all Kripke models \( (S, \leq, \Vdash) \), if \( S \Vdash \Gamma \) then \( S \Vdash \varphi \).
\end{theorem}
\begin{proof}
    Soundness holds by induction.
    For adequacy, suppose \( \Gamma \nvdash_{\mathsf{IPC}} \varphi \).
    Then by completeness of Heyting semantics, there is a Heyting algebra \( H \) and \( H \)-valuation \( v \) such that \( v \vDash_H \Gamma \) but \( v \nvDash_H \varphi \).
    By the previous lemma, there is a Kripke model \( (S, \leq, \Vdash) \) such that \( S \Vdash \Gamma \) but \( S \nVdash \varphi \), contradicting the hypothesis.
\end{proof}
